import java.io.File;
import java.io.FileNotFoundException;
import java.io.PrintWriter;
import java.util.ArrayList;
import java.util.Collections;
import java.util.Iterator;
import java.util.List;
import java.util.Set;

/**
 * 
 * @author Cunxin Jia
 *
 */

public class Background {
	Set<Literal> backgroundSet;
	
	public Background(Set<Literal> backgroundSet) {
		this.backgroundSet = backgroundSet;
	}
	
	/**
	 * Generate RLGG of clauses
	 * @param literal1
	 * @param literal2
	 * @return the RLGG clause
	 */
	public Clause RLGG(Literal literal1, Literal literal2) {
		Clause clause1 = new Clause(literal1, backgroundSet);
		Clause clause2 = new Clause(literal2, backgroundSet);
		Clause reducedRLGG = LGG.reduceClause(LGG.generateLGG(clause1, clause2));
		return reducedRLGG;
	}
	
	/**
	 * Generate RLGG of a set of examples
	 * @param posSet
	 * @return the RLGG clause
	 */
	public Clause RLGG(Set<Literal> posSet) {
		Iterator<Literal> iter = posSet.iterator();
		Clause lggClause = null;
		if(posSet.size() >= 2) {
			Literal literal1 = iter.next();
			Literal literal2 = iter.next();
			lggClause = RLGG(literal1, literal2);
		}
		while(iter.hasNext()) {
			Literal curLiteral = iter.next();
			Clause newClause = new Clause(curLiteral, backgroundSet);
			lggClause = LGG.generateLGG(lggClause, newClause);
		}
		return LGG.reduceClause(lggClause);
	}
	
	public boolean covers(Clause clause, Literal literal) {
		return false;
	}
	
	public Set<Literal> getCoveredSet(Clause clause, Set<Literal> set) {
		File tmpFile = new File(Param.tmpFilePath);
		try {
			PrintWriter output = new PrintWriter(tmpFile);
			output.println(clause.toString());
			output.flush();
			List<Literal> backgroundList = new ArrayList<Literal>();
			backgroundList.addAll(backgroundSet);
			Collections.sort(backgroundList);
			for(int i = 0; i < backgroundList.size(); i++) {
				output.println(backgroundList.get(i).toString() + ".");
				System.out.println(backgroundList.get(i).toString() + ".");
				output.flush();
			}
		} catch (FileNotFoundException e) {
			// TODO Auto-generated catch block
			e.printStackTrace();
		}
		SWIProver prover = new SWIProver(Param.tmpFilePath, set);
		prover.executeQuery();
		return prover.getCoveredSet();
	}
	public int getCoveredNum(Clause clause, Set<Literal> set) {
		File tmpFile = new File(Param.tmpFilePath);
		try {
			PrintWriter output = new PrintWriter(tmpFile);
			output.println(clause.toString());
			output.flush();
			
			List<Literal> backgroundList = new ArrayList<Literal>();
			backgroundList.addAll(backgroundSet);
			Collections.sort(backgroundList);
			for(int i = 0; i < backgroundList.size(); i++) {
				output.println(backgroundList.get(i).toString() + ".");
				System.out.println(backgroundList.get(i).toString() + ".");
				output.flush();
			}
		} catch (FileNotFoundException e) {
			// TODO Auto-generated catch block
			e.printStackTrace();
		}
		SWIProver prover = new SWIProver(Param.tmpFilePath, set);
		return prover.executeQuery();
	}
	
	
//	/**
//	 * Check if a clause covers an example
//	 * @param clause
//	 * @param literal
//	 * @return true if the clause covers the example
//	 */
//	public boolean covers(Clause clause, Literal literal) {
//		if(!clause.getHead().getAtom().getPredicate().equals(literal.getAtom().getPredicate())) {
//			return false;
//		}
//		else {
//			Map<Term,Term> substitution = new HashMap<Term,Term>();
//			List<Term> vars = clause.getHead().getAtom().getTerms();
//			List<Term> consts = literal.getAtom().getTerms();
//			/**
//			 * Substitute variables with corresponding constants
//			 */
//			for(int i = 0; i < vars.size(); i++) {
//				Term curVar = vars.get(i);
//				Term curConsts = consts.get(i);
//				substitution.put(curVar, curConsts);
//			}
//			
//			Iterator<Literal> iter = clause.getBody().iterator();
//			List<Literal> literalsWithVars = new ArrayList<Literal>();
//			while(iter.hasNext()) {
//				Literal curLiteral = iter.next();
//				Literal newLiteral = curLiteral.substitute(substitution);
//				if(newLiteral.isGround()) {
//					if(!backgroundSet.contains(newLiteral)) {
//						return false;
//					}
//				}
//				else {
//					literalsWithVars.add(newLiteral);
//				}
//			}
//			
//			/**
//			 * sort the list by the number of variables the literals contain
//			 */
//			Collections.sort(literalsWithVars);
//			/**
//			 * check if the body of the clause is satisfiable
//			 */
//			List<List<Map<Term,Term>>> literalsWithSubstitutions = new ArrayList<List<Map<Term,Term>>>();
//			for(int i = 0; i < literalsWithVars.size(); i++) {
//				Literal curLiteral = literalsWithVars.get(i);
//				List<Map<Term, Term>> curLiteralWithSubstitutions = getPossibleSubstitutions(curLiteral);
//				literalsWithSubstitutions.add(curLiteralWithSubstitutions);
//			}
//			
//			if(findLegalSubstitution(literalsWithSubstitutions) != null) {
//				return true;
//			}
//			else {
//				return false;
//			}
//		}
//	}
//	
//	/**
//	 * @param literalsWithSubstitutions
//	 * @return
//	 */
//	private Map<Term, Term> findLegalSubstitution(
//			List<List<Map<Term, Term>>> literalsWithSubstitutions) {
//		List<Map<Term, Term>> substitutions1 = literalsWithSubstitutions.get(0);
//		for(int i = 0; i < substitutions1.size(); i++) {
//			Map<Term, Term> curSubsitution = substitutions1.get(i);
//			
//		}
//		return null;
//	}
//
//	private List<Map<Term, Term>> getPossibleSubstitutions(Literal literal) {
//		List<Map<Term,Term>> substitutionList = new ArrayList<Map<Term, Term>> ();
//		Iterator<Literal> iter = backgroundSet.iterator();
//		while(iter.hasNext()) {
//			Literal curLiteral = iter.next();
//			if(curLiteral.getAtom().getPredicate().equals(literal.getAtom().getPredicate())) {
//				List<Term> terms1 = curLiteral.getAtom().getTerms();
//				List<Term> terms2 = literal.getAtom().getTerms();
//				if(terms1.size() == terms2.size()) {
//					Map<Term, Term> substitution = new HashMap<Term, Term> ();
//					int i = 0;
//					for(i = 0; i < terms1.size(); i++) {
//						Term term1 = terms1.get(i);
//						Term term2 = terms2.get(i);
//						if(term1.equals(term2)) {
//							continue;
//						}
//						else if(term1.isConstant() && term2.isConstant() && !terms1.equals(term2)) {
//							break;
//						}
//						else if(term1.isConstant() && !term2.isConstant()) {
//							substitution.put(term2, term1);
//						}						
//					}
//					/**
//					 * the literal is satisfiable by current atom under substitution
//					 * then add the substitution to the list
//					 */
//					if(i == terms1.size()) {
//						substitutionList.add(substitution);
//					}
//				}
//			}
//		}
//		return substitutionList;
//	}

}
